package gov.nasa.jpf.symbc.modelcounter.sampler;

import java.util.Set;

import org.apfloat.Apfloat;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.symbc.modelcounter.sampler.EvaluationVisitor.Result;
import gov.nasa.jpf.symbc.numeric.Constraint;
import gov.nasa.jpf.symbc.numeric.PathCondition;

/**
 * A model counter that "counts" model by sampling that variable space.
 */
public class BruteForceSampler extends Sampler {

	/**
	 * A visitor for constraints/expressions used to determine whether samples
	 * are true or false.
	 */
	protected EvaluationVisitor evaluator;

	/**
	 * Constructor for the sampler. The first step is to read settings from the
	 * given configuration.
	 * 
	 * @param config
	 *            a JPF configuration
	 */
	public BruteForceSampler(Config config) {
		super(config);
		evaluator = new EvaluationVisitor(null);
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * gov.nasa.jpf.symbc.modelcounter.ModelCounter#getConditionalProbability
	 * (gov.nasa.jpf.symbc.numeric.PathCondition, double)
	 */
	@Override
	public Apfloat getConditionalProbability(PathCondition pathCondition,
			Apfloat parentProb) {
		int m = 0; // Number of viable samples.
		int t = 0; // Number of true viable samples.
		// Sample, but never more than sampleLimit times.
		for (int n = 0; n < sampleLimit; n++) {
			sampleCount++;
			Assignment a = new MapAssignment(this);
			Constraint c = pathCondition.header.and;
			while (c != null) {
				evaluator.reset(a);
				c.accept(evaluator);
				if (evaluator.getResult() != Result.TRUE) {
					break;
				}
				c = c.and;
			}
			if (c == null) {
				// Sample a is viable, so evaluate header.
				m++;
				evaluator.reset(a);
				pathCondition.header.accept(evaluator);
				if (evaluator.getResult() == Result.TRUE) {
					t++;
				}
				if (m == nrOfSamples) {
					break;
				}
			}
		}
		// Keep going until we have at least one sample.
		while (m < 1) {
			sampleCount++;
			Assignment a = new MapAssignment(this);
			Constraint c = pathCondition.header.and;
			while (c != null) {
				evaluator.reset(a);
				c.accept(evaluator);
				if (evaluator.getResult() != Result.TRUE) {
					break;
				}
				c = c.and;
			}
			if (c == null) {
				m++;
				evaluator.reset(a);
				pathCondition.header.accept(evaluator);
				if (evaluator.getResult() == Result.TRUE) {
					t++;
				}
			}
		}
		// If m < nrOfSamples here, we have under-sampled, but never mind.
		// System.out.println("prob = " + t + " / " + m);
		return Apfloat.ONE.multiply(new Apfloat(t)).divide(new Apfloat(m));
	}

	@Override
	public Apfloat getProbability(Set<PathCondition> pathConditions) {
		// TODO Auto-generated method stub
		return null;
	}

}
